A1, A2:Type, B1:(A1Type), B2:(A2Type).
strong-subtype(A1;A2)  (a:A1. B1(a)  B2(a))  a:A1 fp B1(a)  a:A2 fp B2(a) 

latex

Definitions	l[i], , AB, A, ||as||, P  Q, {T}, P  Q, P & Q, False, S  T, S  T, (x  l), strong-subtype(A;B), Prop, x:A. B(x), P  Q, A & B, a:A fp B(a), x:A. B(x), x. t(x), x(s), t  T
Lemmas	fpf wf, l member wf, nil member, cons member, select wf, length wf1